home *** CD-ROM | disk | FTP | other *** search
/ Turnbull China Bikeride / Turnbull China Bikeride - Disc 1.iso / ARGONET / PD / PROGRAMMING / LCLINT2.SPK / test / test_a / db3 / lcl / erc < prev    next >
Text File  |  1996-08-28  |  1KB  |  73 lines
  1. imports eref;
  2.  
  3. mutable type erc;
  4.  
  5. only erc erc_create(void) 
  6. {
  7.   /* ensures fresh(result) /\ result' = { }; */
  8. }
  9.  
  10. void erc_clear(erc c) 
  11. {
  12.   /* requires c^.activeIters = 0; */
  13.   modifies c;
  14.   /* ensures c' = { }; */
  15. }
  16.  
  17. void erc_insert(erc c, eref er) 
  18. {
  19.   /* requires c^.activeIters = 0 /\ er \neq erefNIL; */
  20.   modifies c;
  21.   /* ensures c' = [insert(er, c^.val), 0]; */
  22. }
  23.  
  24. | bool : void | erc_delete(erc c, eref er) 
  25. {
  26.   /* requires c^.activeIters = 0; */
  27.   modifies c;
  28.   /* ensures result = er \in c^.val
  29.      /\ c' = [delete(er, c^.val), 0]; */
  30. }
  31.  
  32. bool erc_member(eref er, erc c) 
  33. {
  34.   /* ensures result = er \in c^.val; */
  35. }
  36.  
  37. eref erc_choose(erc c) 
  38. {
  39.   /* requires size(c^.val) \neq 0; */
  40.   /* ensures result \in c^.val; */
  41. }
  42.  
  43. int erc_size(erc c) 
  44. {
  45.   /* ensures result = size(c^.val); */
  46. }
  47.  
  48. void erc_join(erc c1, erc c2) 
  49. {
  50.   /* requires c1^.activeIters = 0; */
  51.   modifies c1;
  52.   /* ensures c1' = [c1^.val \U c2^.val, 0]; */
  53. }
  54.  
  55. only char *erc_sprint(erc c) 
  56. {
  57.   /* ensures isSprint(result[]', c^) /\ fresh(result[]); */
  58. }
  59.  
  60. void erc_final (only erc c) 
  61. {
  62.   modifies c;
  63.   /* ensures trashed(c); */
  64. }
  65.  
  66. void erc_initMod (void) internalState;
  67. {
  68.   modifies internalState;
  69.   ensures true;
  70. }
  71.  
  72. iter erc_elements (erc c, yield eref el);  
  73.